% !TEX root = eventb-fac.tex


\subsection{Safety}
This section generalizes the results of Section \ref{s:types} to the multiparty asynchronous case. In order to lighten the syntax, the types for networks do not include any information on interfaces and only describes an active session. 
Indeed, as interfaces provide information  about the services the location  may execute and  as each location contains a complete collection of processes $\Pool$ then the interface type will be the same for each location.
We have already described how to type a process, we now show how to type its monitor and relatives queues and how to combine them into networks.

As communication is asynchronous the information on the type of a session participant $\pt{p}$ ($\kappa[\pt{p}]$) can be split between the process implementing the session and the associated session queue. We thus talk of \emph{generalized types}, which can be either a message type, a monitor type or the combination of the two. More precisely:

\begin{mydef}
 Session types, generalized types, message and queues types are defined by:
\[
\begin{array}{lccl}
  \text{Session types} & \Delta & ::= & \emptyset ~\sepr~ \Delta, \kappa[\pt{p}]: \chi\\
 \text{Generalized types} & \chi & ::= & \moni{M} ~\sepr~ \mathcal{Q} ~\sepr~ \mathsf{m}\\
 \text{Queue types} & \mathcal{Q} & ::= & \tup{\mathsf{m}, \moni{M} }\\ 
 \text{Message types} & \mathsf{m} & ::= & \epsilon ~\sepr~ q!\lambda(S) ~\sepr~ \mathsf{m};\mathsf{m}
    
\end{array}
\]
The typing judgments for networks  are of  shape
$$ \systype{\Gamma}{\Sigma}{N}{\Delta}
$$
\end{mydef}
where $\Sigma$ lists the free session names in $N$. 
As for the binary case, type safety relies on a notion of balance: communications are performed in the right order and with the proper type. The definition of duality $\bowtie$ is the same as for the binary case (see Definition \ref{def:dualr}).

\begin{mydef}
A session typing $\Delta$ is balanced for the session $\kappa$ (denoted $\con{\Delta, \kappa}$) if $\kappa[\pt{p}]: \chi \in \Delta$ and $\kappa[\pt{q}]: \chi' \in \Delta$ with $\pt{p} \neq \pt{q}$ imply $\proje{\chi}{\pt{q}} \bowtie \proje{\chi'}{\pt{p}}$ where the projection of generalized types onto participants is given in Table \ref{tab:genparticip}.  
\end{mydef}



\begin{table}
  \[
 \begin{array}{c}
  \proje{(p!\lambda(S);m)}{\pt{q}} ~= 
  \begin{cases}
   !\lambda(S).\proje{m}{\pt{q}} & \text{if } \pt{p}=\pt{q}\\
   \proje{m}{\pt{q}} & \text{otherwise}
  \end{cases}
\quad 

\proje{\epsilon}{\pt{q}} = \epsilon 
\quad
\proje{\mathsf{end}}{\pt{q}} = \epsilon
\quad

\proje{\tup{m, \moni{M}}}{\pt{q}} = (\proje{m}{\pt{q}}) . (\proje{\moni{M}}{\pt{q}})

\vspace{2mm} \\
\proje{\pt{p}?\{\lambda_i(S_i).\moni{M}_i\}_{i\in I})}{\pt{q}} ~= 
\begin{cases}
 ?\{ \lambda_i(S_i).(\proje{\moni{M}_i}{\pt{q}})\}_{i\in I} & \text{if } \pt{p}=\pt{q}\\
 \proje{\moni{M}_k}{\pt{q}} & \text{where } k \in I, \pt{p}\neq\pt{q} \text{ and } \forall i, j \in I \ \moni{M}_i = \moni{M}_j
\end{cases}
\vspace{2mm} \\

\proje{\pt{p}!\{\lambda_i(S_i).\moni{M}_i\}_{i\in I})}{\pt{q}} ~= 
\begin{cases}
 !\{ \lambda_i(S_i).(\proje{\moni{M}_i}{\pt{q}})\}_{i\in I} & \text{if } \pt{p}=\pt{q}\\
 \proje{\moni{M}_k}{\pt{q}} & \text{where } k \in I, \pt{p}\neq\pt{q} \text{ and } \forall i, j \in I \ \moni{M}_i = \moni{M}_j
\end{cases}

 \end{array}
\]
\caption{Projection of generalized types onto participants}\label{tab:genparticip}
\end{table}

% \begin{mydef}[Duality]
%  Projection of generalized types
%  \[ \Theta ::=  !\lambda(S) \sepr \Theta.\Theta \sepr ?\{\Theta_i\}_i\in I \sepr !\{\Theta_i\}_i\in I \sepr \epsilon
%  \]
%  
% 
% \[ 
% \begin{array}{l}
% \epsilon \bowtie \epsilon \\
% 
% \text{If } \Theta \bowtie \Theta_j \text{ with } j \in I \text{ then } !\lambda_j(S_j).\Theta \bowtie ?\{\lambda_i(S_i).\Theta_i\}_{i\in I} \\
% 
% \text{If } \forall i\in I \ \Theta_i \bowtie \Theta_i' \text{ then } !\{\lambda_i(S_i).\Theta_i\}_{i\in I} \bowtie ?\{\lambda_i(S_i).\Theta_i'\}_{i\in I} \\
% 
% \text{If } \Theta_1 \bowtie \Theta_2  \text{ and } \Theta_3 \bowtie \Theta_4 \text{ then } \Theta_1.\Theta_3 \bowtie \Theta_2.\Theta_4
% 
% \end{array}
%  \]
%  
%  
% \end{mydef}

It is easy to see that session types obtained from the projection of global types are balanced.

\begin{proposition}\label{prop:global}
 Let $\gtype{G}$ be a global type and $\pt{p} \neq \pt{q}$, then 
 $\proje{(\proje{\gtype{G}}{\pt{p}})}{\pt{q}} \,\bowtie \, \proje{(\proje{\gtype{G}}{\pt{q}})}{\pt{p}}$.
\end{proposition}

\begin{table}

\[
\begin{array}{c}
\inferrule*[right=\rulename{M:New}]
{\quad}{\systype{\Gamma}{\emptyset}{\new(G)}{\emptyset} }
\qquad

\inferrule*[right=\rulename{M:End}]
{\quad}{\systype{\Gamma}{\emptyset}{\monpro{\mathsf{end}}{P}}{\emptyset} }
\qquad

\inferrule*[right=\rulename{M:MP}]
{\multyping{\Gamma}{P}{\kappa[\pt{p}]: T} \\ 
 \moni{M} \neq \mathsf{end}\\
  T \propto \moni{M}}
{\systype{\Gamma}{\emptyset}{\monpro{\moni{M}}{P}}{\kappa[\pt{p}]: \moni{M}}}
\vspace{2mm}\\

\inferrule*[right=\rulename{M:CQueue}]{\quad}
{\systype{\Gamma}{\emptyset}{\que{\kappa^{e}}{h}}{\emptyset}}
\qquad

\inferrule*[right=\rulename{M:QInit}]
{\quad }
{\systype{\Gamma}{\{\kappa\}}{\kappa:\emptyset}{\emptyset}}
\qquad
\inferrule*[right=\rulename{M:QSend}]
{\systype{\Gamma}{\{\kappa\}}{\kappa:h}{\Delta}\\
\Gamma \vdash v:S}
{\systype{\Gamma}{\{\kappa\}}{\kappa:(\pt{p},\pt{q},\lambda(v))\cdot h}{\Delta\#\{ \kappa[\pt{p}]: \pt{q}!\lambda(S)\}}}
\vspace{2mm}\\

\inferrule*[right=\rulename{M:Par}]
{\systype{\Gamma}{\Sigma_1}{N_1}{\Delta_1}\\
\systype{\Gamma}{\Sigma_2}{N_2}{\Delta_2}}
{\systype{\Gamma}{\Sigma_1 \cup \Sigma_2}{N_1 \para N_2}{\Delta_1 \star \Delta_2} }
\quad  

\inferrule*[right=\rulename{M:Equiv}]
{\systype{\Gamma}{\Sigma}{N}{\Delta} \\ \Delta \approx \Delta'}
{\systype{\Gamma}{\Sigma}{N}{\Delta'} }
\qquad

\inferrule*[right=\rulename{M:Res}]
{\systype{\Gamma}{\Sigma}{N}{\Delta} \\ \con{\Delta,\kappa}}
{\systype{\Gamma}{\Sigma \setminus \{\kappa\}}{\restr{\kappa}{N}}{\Delta \setminus \{\kappa\}} }
\vspace{2mm}\\

\inferrule*[right=\rulename{M:Loc1}]
{\forall (P, T_P) \in \Pool \quad  \multyping{\Gamma}{P}{T_P} }
{\systype{\Gamma}{\emptyset}{\scomponent{\locf{loc}}{\Pool ; \que{\locf{loc}}{r} }}{\emptyset} }
\qquad

\inferrule*[right=\rulename{M:Loc2}]
{\forall (P, T_P) \in \Pool \quad  \multyping{\Gamma}{P}{T_P} \\
\systype{\Gamma}{\emptyset}{\monpro{\moni{M}}{P}}{\kappa[\pt{p}]: \moni{M}}}
{\systype{\Gamma}{\emptyset}{\scomponent{\locf{loc}}{\monpro{\moni{M}}{P};\Pool ; \que{\locf{loc}}{r} }}{\kappa[\pt{p}]: \moni{M}} }


\end{array}
\]

\caption{Typing rules for networks and queues}\label{tab:typesnet}
\end{table}

We are now ready to complete the typing system with the typing rules for networks and queues, which are given in Table \ref{tab:typesnet}.
A session initiator is typed with the empty session typing. If $\moni{M}=\mathsf{end}$ a monitored process $\monpro{\moni{M}}{P}$ is  typed to the empty session type otherwise if the type of $P$ ($\kappa[\pt{p}]: T$) is adequate with respect to the monitor than the type of the monitored process is $\kappa[\pt{p}]: \moni{M}$.
The event queue $\kappa^e$ is typed with the completed session type. Rules \rulename{M:Qinit} and \rulename{QSend} type the session message queue. In particular, rule \rulename{Qsend} makes use of the operator $\#$ that dispatches message types to proper session channels:
\[
\begin{array}{lcl}
 m\#m' &::= &m;m'\\
 
 \Delta \# \Delta'& ::= &\{ \kappa[\pt{p}] : \chi \# \chi' \mid  \kappa[\pt{p}]: \chi \in \Delta  \wedge \kappa[\pt{p}]: \chi' \in \Delta'\} \cup \{\kappa[\pt{p}] : \chi \mid  \kappa[\pt{p}]: \chi \in \Delta \cup \Delta'  \wedge \kappa[\pt{p}]: \chi \notin \Delta \cap \Delta'\} \\
\end{array}
 \]
Rule \rulename{M:Par} combines networks; in particular,
it relies on 
 operator $\star$, which combines the typing information coming from queues and monitored processes:
\[
\begin{array}{lcl}
 
 m \star \moni{M} &::=& \tup{m,\moni{M}} \\
 \moni{M} \star m &::=& \tup{m,\moni{M}} \\
 
 \Delta \star \Delta'& ::= &\{ \kappa[\pt{p}] : \chi \star \chi' \mid  \kappa[\pt{p}]: \chi \in \Delta  \wedge \kappa[\pt{p}]: \chi' \in \Delta'\} \cup \{\kappa[\pt{p}] : \chi \mid  \kappa[\pt{p}]: \chi \in \Delta \cup \Delta'  \wedge \kappa[\pt{p}]: \chi \notin \Delta \cap \Delta'\} \\
\end{array}
\]

In order to take into account the structural congruence on queues (rule \rulename{M:Equiv}) we build an equivalence relation ($\approx$) on types that is induced by the following equivalence rule on message types:
 \[
 m;\pt{q}!\lambda(S);\pt{q}'!\lambda(S');m' \approx  m;\pt{q}'!\lambda(S');\pt{q}!\lambda(S);m' 
 \]
with $\pt{q} \neq \pt{q}'$, and is extended to generalized types by letting
\[ \text{if } m \approx m' \text{ then } \tup{m, \moni{M}} \approx \tup{m', \moni{M}}.\]

As expected, the type of a restricted network (rule \rulename{M:Res}) depends on the consistency of the session $\kappa$. Finally, rules~\rulename{M:Loc1} and \rulename{M:Loc2} are used to type locations: as in the binary case, locations do not add any information to the session type.


We conclude this section with the proof of the \emph{subject reduction} theorem,
which guarantees that communications 
are performed by (located) monitored process 
in a safe manner, following the protocols prescribed by global types.
It basically generalizes to the multiparty case the proof given for binary session types; see Appendix~\ref{app:proofs} for details of the proof.

\begin{mytheo}[Subject Reduction]\label{th:multisubred}
If $\systype{\Gamma}{\Sigma}{N}{\Delta}$ with $\Delta$ balanced and $N \pired N'$ then $\systype{\Gamma}{\Sigma}{N'}{\Delta'}$, for some balanced~$\Delta'$.
\end{mytheo}

Notice that we can also prove a form of \emph{progress}: i.e., in the absence of internal adaptation events (only external adaptation), every input monitored process will eventually receive a message and conversely every message in a queue will eventually be received by an input monitored process.\footnote{The restriction to external adaptation is expected, as as internal updates are meant to modify the protocol for current participants, and so sent messages could be left undelivered. }
The proof is similar to the one presented in \cite{CDV15j}, which crucially depends on the assumption that 
a process owns only one session channel.
%session are not interlaced and thus it would not hold in the generalized scenario.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

We now extend \emph{safety} and \emph{consistency} properties to the multiparty case. Similarly as before we define  \emph{$\kappa$-redexes}, 
and \emph{error processes}. Major changes are due to the fact that here we assume asynchronous communication.


\begin{mydef}[$\kappa$-redexes, errors]\label{d:multikred}
A network $N$ contains a \emph{$\kappa$-redex} if it is of one the following forms:
%\[ \begin{array}{c}
%\eval{\scomponent{\locf{loc_{\pt{p}}}}{\monpro{\moni{M}_{in}}{\kappa[\pt{p}]?\{\lambda_i(x_i).P_i\}_{i\in I} };\Pool_{\pt{p}} ; \que{loc_{\pt{p}}}{r} } \para \scomponent{\locf{loc_{\pt{q}}}}{\monpro{\moni{M}_o}{\kappa[\pt{q}]!\lambda(v).P };\Pool_{\pt{q}} ; \que{loc_{\pt{q}}}{r'} }} \\
%\text{or} \\
%\eval{\scomponent{\locf{loc}}{\monpro{\moni{M}_{in}}{\kappa[\pt{p}]?\{\lambda_i(x_i).P_i\}_{i\in I} };\Pool ; \que{loc}{r} } \para \kappa: (\pt{q},\pt{p},\lambda(v))\cdot h} \\
%\end{array}
%\]

\begin{enumerate}[(a)]
\item $\eval{\scomponent{\locf{loc_{\pt{p}}}}{\monpro{\moni{M}_{in}}{\kappa[\pt{p}]?\{\lambda_i(x_i).P_i\}_{i\in I} };\Pool_{\pt{p}} ; \que{loc_{\pt{p}}}{r} } \para \scomponent{\locf{loc_{\pt{q}}}}{\monpro{\moni{M}_o}{\kappa[\pt{q}]!\lambda(v).P };\Pool_{\pt{q}} ; \que{loc_{\pt{q}}}{r'} }} $
\item $\eval{\scomponent{\locf{loc}}{\monpro{\moni{M}_{in}}{\kappa[\pt{p}]?\{\lambda_i(x_i).P_i\}_{i\in I} };\Pool ; \que{loc}{r} } \para \kappa: (\pt{q},\pt{p},\lambda(v))\cdot h} $
\end{enumerate}
where 
$\moni{M}_{in} = p?\{\lambda_i(S_i).\moni{M}_i\}_{i\in I} $, $\moni{M}_o = p! \lambda(S).\moni{M'}$
and there exists $j \in I$ such that $\lambda_j = \lambda$ and $S_j = S$.

A network $N \equiv (\nu \til{\kappa})(N')$ is an \emph{error} if $N'$ contains a $\kappa$-redex.
\end{mydef}

The introduction of internal updates breaks the update-consistency property as stated in Section \ref{s:types}. This is expected as internal updates are meant to globally change the communication protocol agreed upon session establishment. Nonetheless as external updates behaves exactly as in the binary case the property is preserved for them.

We, thus, generalize the properties of safety and consistency:

\begin{mydef}[Safety and Consistency]\label{d:multiconsis}
Let $N$ be a network.
\begin{enumerate}[$-$]
\item We say $N$ is \emph{safe} if it never reduces into an error. 
\item We say $N$ is \emph{external update-consistent} 
if and only if,
 for all  $\kappa$ such that $N$ contains a $\kappa$-redex, 
if $N \pired N'$ and rule \rulename{N:Updloc} has been used to derive $\pired$
then $N'$ contains the same $\kappa$-redex.
\end{enumerate}
\end{mydef}


As before  our main result follows as a  consequence of Theorem~\ref{th:multisubred}.
 
\begin{mytheo}[Typing Ensures Safety and Consistency]\label{t:multisafety}
If $\systype{\Gamma}{\Sigma}{N}{\Delta}$ with $\Delta$ balanced
then network $N$ is safe and external update consistent.
\end{mytheo}









%\subsection{Philosophy}
%
%0) i tipi globali hanno degli indirizzi per specificare dove cercare il processo
%
%
%1) separate session code from adaptation code
%
%2) locations are containers
%  if no session is active (has been opened) the location contains a pool of processes $(P_i, T_i)_{i \in 1..m}$, a queue (that will be used to receive external update events), a code to manage adaptation events \jp{where is this code in the rule?} (?? I am not sure this is necessary, it can be used to relax our discipline, for the moment I assume that for all locations all adaptation events are processed in a prioritary way as soon as they appear in the adaptation queues, ie no other action is possible if those queues contains a message) 
%
% 3) location can only have one opened session chosen among the pool of processes, the rest of the processes in the pool remains available for eventual internal adaptation.
%  Once a session is opened locations contains: \\
%i) the implementation of the session (ie $P_j$), \\
%ii) its monitor (ie current state/type of the session),\\
%iii) the messages queue for the session (ie $k_j$ that manages asynchronous communication among participants of the session) \\
%iv) the events queue for the session (ie $k^e_j$ that receives internal adaptation events) \\
%v) the rest of the pool of processes (ie $(P_i, T_i)_{i \in 1..m}$ without process $P_j$) \\
%vi) the loc queue mentioned above \jp{ for external updates, right?}\\
%
%4) a system is the parallel composition of a pool of location with no active session $\cal{P}$ and a pool of "active" location $\cal{P}*$
%  in principle when a session is opened it is moved from $\cal{P}$ to $\cal{P}*$ and similarly when the session is closed (ie the monitor reaches $\epsilon$ queues should be emptied and loc returns to $\cal{P}$ (a sort of garbage collector)
%  
%%\end{verbatim}

